A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
(can-apply(f o g  ;x))  {(can-apply(g;x)) & (can-apply(f;do-apply(g;x)))} 

latex

ProofTree

Definitions	False, t  T, P & Q, P  Q, Void, x:A.B(x), Top, x:AB(x), x:A. B(x), S  T, do-apply(f;x), left + right, suptype(S; T), b, True, , A, b, s = t, , x:A  B(x), P  Q, Unit, {T}, Type, can-apply(f;x)
Lemmas	can-apply-compose-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, assert wf, can-apply wf, do-apply wf, false wf